% define page layout
\setlength{\textwidth}{5.7in}
\setlength{\textheight}{8.5in}
%\setlength{\topmargin}{-0.125in}
\setlength{\oddsidemargin}{18pt}
\setlength{\evensidemargin}{18pt}
%\setlength{\columnseprule}{.4pt}
\setlength{\headheight}{19pt}
\setlength{\headsep}{18pt}
%\setlength{\footheight}{16pt}
%\setlength{\footskip}{34pt}
%\setlength{\headrulewidth}{2pt}
%\setlength{\footrulewidth}{0pt}

\renewcommand{\sectionmark}[1]{ }
\renewcommand{\subsectionmark}[1]{ }


%% FILE: holmac.tex
%% This is a LaTeX macro for formatting HOL theory generated by the latex-hol
%% library function
%% By Wai Wong on 21 May 1991
%%

% check to see if this macro file has already been loaded
\ifx\undefined\holmacs\def\holmacs{}\else\endinput\fi

% Special symbols

\def\US{\_}
\def\SH{\#}
\def\AM{\&}
\def\PC{\%}
\def\DO{\$}
\def\BS{{\tt\char'134}}
\def\PR{{\tt\char'23}}
\def\TI{{\tt\char'176}}
\def\AS{{\tt\char'52}}
\def\LE{{\tt\char'74}}
\def\BA{{\tt\char'174}}
\def\GR{{\tt\char'76}}
\def\LB{{\tt\char'133}}
\def\RB{{\tt\char'135}}
\def\CI{{\tt\char'136}}
\def\LC{{\tt\char'173}}
\def\RC{{\tt\char'175}}

\def\GOAL{\relax\ifmmode\hbox{?\kern0.2em --}\quad\else\hbox{?kern0.2em --}\quad\fi}
\def\THM{\relax\ifmmode\vdash\else$\vdash$\fi}
\def\DEF{\relax\ifmmode\vdash\!\!\lower .5ex\hbox{{\scriptsize\sl def}}\quad%
 \else$\vdash\!\!\lower.5ex\hbox{{\scriptsize\sl def}}\quad$\fi}
\def\AND{\relax\ifmmode\wedge\else$\wedge$\fi}
\def\OR{\relax\ifmmode\vee\else$\vee$\fi}
\def\IMP{\relax\ifmmode\supset\else$\supset$\fi}
\def\LONG{\relax\ifmmode\longrightarrow\else$\longrightarrow$\fi}
\def\IFF{\relax\ifmmode\Longleftrightarrow\else$\Longleftrightarrow$\fi}
\def\LEE{\relax\ifmmode\leq\else$\leq$\fi}
\def\GEE{\relax\ifmmode\geq\else$\geq$\fi}
\def\EXISTSUNIQUE{\relax\ifmmode\exists\forall\else$\exists\forall$\fi}
\def\LES{\relax\ifmmode<\else$<$\fi}
\def\GRE{\relax\ifmmode>\else$>$\fi}
\def\MUL{\relax\ifmmode\times\else$\times$\fi}
\def\NOT{\relax\ifmmode\neg\else{$\neg$}\fi}
\def\FORALL{\relax\ifmmode\forall\else$\forall$\fi}
\def\EXISTS{\relax\ifmmode\exists\else$\exists$\fi}
\def\SELECT{\relax\ifmmode\varepsilon\else$\varepsilon$\fi}
\def\FUNCOM{\relax\ifmmode\circ\else$\circ$\fi}
\def\LAMBDA{\relax\ifmmode\lambda\else$\lambda$\fi}
\def\RESDOT{\relax\ifmmode::\else$::$\fi}
\def\DOT{\relax\ifmmode.\,\else$.\,$\fi}
\def\NIL{\relax\ifmmode[\:]\else$[\:]$\fi}
\def\EMPTYSET{\relax\ifmmode{\{\:\}}\else{$\{\:\}$}\fi}
\def\BEGINSET{\relax\ifmmode\left\{\else{$\left\{\right.$}\fi}
\def\ENDSET{\relax\ifmmode\right\}\else{$\left.\right\}$}\fi}
\def\SUCHTHAT{\relax\ifmmode\mid\else$\mid$\fi}

%\def\makeulactive{\catcode`\_=\active\relax}
%\def\makeulsub{\catcode`\_=8\relax}
%\let\ul=\_
%\begingroup
% \makeulactive
% \gdef\_{\ul}
% \gdef_{\ul}
%\endgroup
%\def\dotoken#1#2{\mbox{#1#2}\endgroup}
%\def\mlname{\begingroup\makeulactive\dotoken{\tt}}
%\def\CONST{\begingroup\makeulactive\dotoken{\constfont}}
%\def\KEYWD{\begingroup\makeulactive\dotoken{\keyfont}}

\def\HOL{{\sc HOL}}
% Tells TeX to break line after binary operators.
\def\setholprec{\relpenalty=10000 \binoppenalty=9999 \raggedright}

% The parents and types sections are set in ttlist environment
\newenvironment{ttlist}{\begingroup\typefont}{\endgroup}

% The constants and infix sections are set in typelist environment.
% The labels are left justified.
\def\labeledlabel#1{#1\hfil}
\newenvironment{typelist}%
        {\begin{list}{\ }%
        {\typefont \setlength{\leftmargin}{0.8in}%
         \setlength{\labelwidth}{0.7in}\setlength{\labelsep}{0.1in}%
        \renewcommand{\makelabel}{\labeledlabel}}}%
        {\end{list}}

% The Axioms, definitions and theorems sections are set in thmlist environment
\newenvironment{thmlist}
        {\begin{list}{\ }%
        {\setholprec \setlength{\leftmargin}{0.8in}%
         \setlength{\labelwidth}{0.7in}\setlength{\labelsep}{0.1in}%
        \renewcommand{\makelabel}{\labeledlabel}}}%
        {\end{list}}


\def\monthname{\ifcase\month
v  \or Jan\or Feb\or Mar\or Apr\or May\or Jun%
  \or Jul\or Aug\or Sep\or Oct\or Nov\or Dec\fi}%
\def\timestring{\begingroup
   \count0 = \time \divide\count0 by 60
   \count2 = \count0 % the hour
   \count4 = \time \multiply\count0 by 60
   \advance\count4 by -\count0 % the minute
   \ifnum\count4<10 \toks1 = {0}% get a leading zero
   \else            \toks1 = {}%
   \fi
   \ifnum\count2<12 \toks0 = {a.m.}%
   \else            \toks0 = {p.m.}%
        \advance\count2 by -12
   \fi
   \ifnum\count2=0 \count2 = 12 \fi
   \number\count2:\the\toks1 \number\count4
   \thinspace \the\toks0
\endgroup}%
\def\timestamp{\number\day\space\monthname\space
   \number\year\quad\timestring}%
\def\printtimestamp{Printed at \timestring\space%
   on \number\day\space\monthname\space\number\year.}

% The following  commands are generated by latex_theory_to
% They may be redefined to suit your style.
% \sec{section_name} marks the sections within a theory, e.g., Types, Theorems.
% \theory{theory_name} marks the beginning of the theory, if the file is
%       generated for being included in other LaTeX files.
% \endthy{theory_name} marks the end of the theory.
%
\def\sec#1{\section*{#1}\noindent}
\def\theory#1{\section{#1}}
\def\endthy#1{\hbox to\hsize{\hrulefill\ End of theory {\tt#1}\ \hrulefill}}

\def\typefont{\tt}      % for types, ML identifiers
\def\constfont{\sf}     % for HOL constants
\def\keyfont{\bf}       % for keywords



\makeatletter
\def\verb{\begingroup \catcode``=13 \@noligs
\verbatim@font \let\do\@makeother \dospecials
\@ifstar{\@sverb}{\@verb}}

% Definitions of \@sverb and \@verb changed so \verb+ foo+  does not lose
% leading blanks when it comes at the beginning of a line.
% Change made 24 May 89. Suggested by Frank Mittelbach and Rainer Sch\"opf.
%
\def\@sverb#1{\def\@tempa ##1#1{\leavevmode\null##1\endgroup}\@tempa}

\def\@verb{\@vobeyspaces \frenchspacing \@sverb}

\def\wordn{\verb|:word|$n$}
\def\word{\@ifnextchar[{\@word}{\@word[*]}}
\def\@word[#1]{\verb|:(#1)word|}
\def\sect{\@startsection {subsection}{1}{\z@}{-3.5ex plus -1ex minus
 -.2ex}{1.5ex plus .2ex}{\normalsize\bf}}
\def\subsect{\@startsection {subsubsection}{2}{\z@}{-3.5ex plus -1ex minus
 -.2ex}{-1em}{\footnotesize\bf}}
\def\inputmlfile#1{\begingroup \footnotesize \input#1 \endgroup}

\renewenvironment{theindex}{\begin{multicols}{2}[\section*{\indexname}]%
 \columnseprule \z@ \columnsep 35\p@
 \parindent\z@ \parskip\z@ plus.3\p@\relax\let\item\@idxitem}{\end{multicols}}

\def\@idxitem{\par\hangindent 40\p@}

\def\subitem{\par\hangindent 40\p@ \hspace*{20\p@}}

\def\subsubitem{\par\hangindent 40\p@ \hspace*{30\p@}}

\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}

\makeatother


\def\NBWORD#1#2{\CONST{NBWORD}\,\CONST{#1}\,\CONST{#2}}
\def\SEG#1#2#3{\CONST{SEG}\,\CONST{#1}\,\CONST{#2}\,#3}
\def\T{\CONST{T}}

\def\dotoken#1#2{\mbox{#1#2}\endgroup}
\def\idxname#1{\begingroup\makeulother\dotoken#1}
\def\dotokenidx#1#2{\mbox{#1#2}\index{#2@\string\idxname{#1}{#2}}\endgroup}
\def\mlname{\begingroup\makeulother\dotokenidx{\tt}}
\def\CONST{\begingroup\makeulother\dotokenidx{\constfont}}
\def\KEYWD{\begingroup\makeulother\dotoken{\keyfont}}

\def\idxmlname{\begingroup\makeulother\dotoken{\tt}}
\def\idxconst{\begingroup\makeulother\dotoken{\constfont}}
\def\ul#1{\relax\ifmmode\underline#1\else$\underline{#1}$\fi}

% define environment for HOL definitions and theorems
\def\makeulother{\catcode`\_=12\relax}
\def\makeulsub{\catcode`\_=8\relax}
%\begingroup
% \makeulother
% \gdef\_{\ul}
%\endgroup
\def\doholdef#1{\par\vspace*{5pt}\index{#1@\string\idxmlname{#1}|ul}%
 \flushleft{\bf HOL Definition }({\tt#1})\label{def-#1}\endgroup}
\def\holdef{\begingroup\makeulother\doholdef}
\let\endholdef=\endflushleft

\def\doholthm#1{\par\index{#1@\string\idxmlname{#1}|ul}%
 \flushleft{\bf HOL Theorem }({\tt#1})\label{thm-#1}\endgroup}
\def\holthm{\begingroup\makeulother\doholthm}
\let\endholthm=\endflushleft

\def\sfc\sf \def\constfont{\sfc}
